<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>LogicFormula</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="LogicFormula";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Messages.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/LogicFormula.html" target="_top">Frames</a></li>
<li><a href="LogicFormula.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class LogicFormula" class="title">Class LogicFormula</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/Formula.html" title="class in mmj.lang">mmj.lang.Formula</a></li>
<li>
<ul class="inheritance">
<li>mmj.lang.LogicFormula</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">LogicFormula</span>
extends <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a></pre>
<div class="block">LogicFormula is a convenience class for LogHyp.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/LogicFormula.html#LogicFormula(int, mmj.lang.Sym[])">LogicFormula</a></strong>(int&nbsp;workCnt,
            <a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]&nbsp;workFormula)</code>
<div class="block">Construct using count and Sym array.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/LogicFormula.html#LogicFormula(java.util.Map, java.lang.String, java.util.List, java.util.List)">LogicFormula</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
            java.lang.String&nbsp;typS,
            java.util.List&lt;java.lang.String&gt;&nbsp;symList,
            java.util.List&lt;<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;exprHypList)</code>
<div class="block">Construct using String Type Code and Sym List.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicFormula.html#verifyExprSymsDefAndActive(java.util.Map, java.util.List, java.util.List)">verifyExprSymsDefAndActive</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
                          java.util.List&lt;java.lang.String&gt;&nbsp;symList,
                          java.util.List&lt;<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;hypList)</code>
<div class="block">Verifies that each Sym id in Expression is active and accumulates the
 matching VarHyp's in the input exprHypList param.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.Formula">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a></h3>
<code><a href="../../mmj/lang/Formula.html#accumHypInList(java.util.List, T)">accumHypInList</a>, <a href="../../mmj/lang/Formula.html#buildMandVarHypArray(mmj.lang.Hyp[])">buildMandVarHypArray</a>, <a href="../../mmj/lang/Formula.html#buildRuleFormatExpr(mmj.lang.VarHyp[])">buildRuleFormatExpr</a>, <a href="../../mmj/lang/Formula.html#computeWidthOfWidestExprCnst()">computeWidthOfWidestExprCnst</a>, <a href="../../mmj/lang/Formula.html#constructTempDummyFormula(mmj.lang.Cnst, java.lang.String)">constructTempDummyFormula</a>, <a href="../../mmj/lang/Formula.html#equals(java.lang.Object)">equals</a>, <a href="../../mmj/lang/Formula.html#exprEquals(java.lang.Object)">exprEquals</a>, <a href="../../mmj/lang/Formula.html#exprToString()">exprToString</a>, <a href="../../mmj/lang/Formula.html#getCnt()">getCnt</a>, <a href="../../mmj/lang/Formula.html#getExpr()">getExpr</a>, <a href="../../mmj/lang/Formula.html#getParseNodeHolderExpr(mmj.lang.Hyp[])">getParseNodeHolderExpr</a>, <a href="../../mmj/lang/Formula.html#getParseNodeHolderExpr(mmj.lang.VarHyp[])">getParseNodeHolderExpr</a>, <a href="../../mmj/lang/Formula.html#getSym()">getSym</a>, <a href="../../mmj/lang/Formula.html#getTyp()">getTyp</a>, <a href="../../mmj/lang/Formula.html#hashCode()">hashCode</a>, <a href="../../mmj/lang/Formula.html#setTyp(mmj.lang.Cnst)">setTyp</a>, <a href="../../mmj/lang/Formula.html#setTyp(java.util.Map, java.lang.String)">setTyp</a>, <a href="../../mmj/lang/Formula.html#srcStmtEquals(mmj.mmio.SrcStmt)">srcStmtEquals</a>, <a href="../../mmj/lang/Formula.html#toProofWorksheetStringBuilder(java.lang.StringBuilder, int, int)">toProofWorksheetStringBuilder</a>, <a href="../../mmj/lang/Formula.html#toString()">toString</a>, <a href="../../mmj/lang/Formula.html#toStringBuilderLineList(java.util.List, java.lang.StringBuilder, int, int, java.lang.String)">toStringBuilderLineList</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="LogicFormula(int, mmj.lang.Sym[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>LogicFormula</h4>
<pre>public&nbsp;LogicFormula(int&nbsp;workCnt,
            <a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]&nbsp;workFormula)</pre>
<div class="block">Construct using count and Sym array.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workCnt</code> - length of formula.</dd><dd><code>workFormula</code> - Formula Sym array.</dd></dl>
</li>
</ul>
<a name="LogicFormula(java.util.Map, java.lang.String, java.util.List, java.util.List)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>LogicFormula</h4>
<pre>public&nbsp;LogicFormula(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
            java.lang.String&nbsp;typS,
            java.util.List&lt;java.lang.String&gt;&nbsp;symList,
            java.util.List&lt;<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;exprHypList)
             throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct using String Type Code and Sym List.
 <p>
 Verifies that each Sym id in Expression is active and accumulates the
 matching VarHyp's in the input exprHypList param.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symTbl</code> - Symbol Table (map).</dd><dd><code>typS</code> - Formula Type Code String.</dd><dd><code>symList</code> - Formula Expression as List of Sym id Strings</dd><dd><code>exprHypList</code> - List of Hyps, updated in function.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="verifyExprSymsDefAndActive(java.util.Map, java.util.List, java.util.List)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>verifyExprSymsDefAndActive</h4>
<pre>public&nbsp;void&nbsp;verifyExprSymsDefAndActive(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
                              java.util.List&lt;java.lang.String&gt;&nbsp;symList,
                              java.util.List&lt;<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;hypList)
                                throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Verifies that each Sym id in Expression is active and accumulates the
 matching VarHyp's in the input exprHypList param.
 <p>
 <ol>
 <li>verify that each symbol string in an expression is defined and
 active, and that each referenced variable is defined by an active
 variable hypothesis (in scope). NOTE: this routine is not used for
 disjoint variables because they do not have "expressions" as such, and
 also, they may not have active variable hypotheses.
 <li>build a Sym[] as the symbol strings are scanned, thus converting the
 source strings to unique object references.
 <li>while building Sym[], build the set of variable hypotheses for the
 variables in the expression, and store them in the input hypList.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symTbl</code> - Map containing Cnst and Var definitions.</dd><dd><code>symList</code> - expression's symbol character strings</dd><dd><code>hypList</code> - List of Hyp's. Is updated with unique variable hypotheses
            in the expression. Because the list is maintained in database
            statement sequence order, hypList should either be empty (new)
            before the call, or already be in that order (see
            <code>accumHypInList</code>.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate symbol, etc. (see
             <code>mmj.lang.LangConstants.java</code>)</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Messages.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/LogicFormula.html" target="_top">Frames</a></li>
<li><a href="LogicFormula.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
